Codex Code Review

1. Critical – Constraint soundness regression in CPU byte range checks
   In cpu.rs:1967 and cpu.rs:514, the PR replaces per-byte IS_BYTE checks with halfword checks on b_lo + 256*b_hi.
   This does not prove each byte column is in [0,255] (e.g. b_lo=257, b_hi=0 still gives a valid halfword value 257). So byte columns become non-canonical while still satisfying packed-word constraints like constraints/cpu.rs:28.
   Impact: this can invalidate assumptions elsewhere (notably byte-sum zero logic used by BEQ in cpu.rs:1157) and weakens VM proof soundness.

   Action: keep IS_BYTE checks for ARG1/ARG2/RES bytes (or add equivalent explicit per-byte constraints). IS_HALF can be additive, but not a replacement for byte range checks here.

No other significant security/bug/performance issues stood out in the diff.

/bench

Benchmark — fib_iterative_8M (median of 3)

_{Table parallelism: 32 (auto = cores / 3)}

🎉 Improvement detected — heap or time decreased by more than 5%.

✅ Low variance (time: 2.2%, heap: 4.5%)

_{Commit: 18b8424 · Baseline: cached · Runner: self-hosted bench}

Review summary

One security concern (inline) and two stale comments.

Stale comments not updated by this PR

prover/src/tables/cpu.rs:39 — module doc still lists IS_BYTE for arg1/arg2/res:

-//! - IS_BYTE: range checks for rs1, rs2, rd, arg1[i], arg2[i], res[i]
+//! - IS_BYTE: range checks for rs1, rs2, rd
+//! - IS_HALF: range checks for arg1[2i]+256*arg1[2i+1], arg2[2i]+256*arg2[2i+1], res[2i]+256*res[2i+1] (i=0..3)

prover/src/tables/cpu.rs:536 — comment inside collect_bitwise_ops still says 27 IS_BYTE:

-        // Byte range checks: 27 IS_BYTE
+        // Range checks: 3 IS_BYTE + 12 IS_HALF = 15 ops

The main security concern is filed as an inline comment on line 515 (the incorrect claim that IS_HALF implies per-byte range). These two lines were not in the diff so couldn't be filed inline.

/bench 5

/bench 3

/bench

Codex Code Review

1. High – Protocol/compatibility break from BusId renumbering
   In types.rs:52 and types.rs:152-171, IsB20 was changed from ID 2 to 3, which shifts every subsequent bus ID by +1 and leaves 2 unused.
   This changes the bus fingerprints for all affected interactions, so any component expecting previous numeric IDs (persisted proofs, external verifier, cross-version validation) will fail or become incompatible.

   Actionable fix: keep existing bus numeric assignments stable (restore IsB20 = 2 and old TryFrom<u64> mapping), unless this PR explicitly introduces a versioned protocol migration across prover/verifier.

No other concrete security/correctness/performance issues stood out in the diffed changes.

Test gap: I could not run cargo tests in this environment because rustup failed to create temp files on a read-only path.

Review

Soundness: previous "Critical" concern was a false positive

Both the first Codex comment and the previous Claude inline were based on a misread of the approach. The concern was about IS_HALF-style packing (b_lo + 256*b_hi → single bus value), which genuinely wouldn't prove per-byte range. But that's not what the PR does.

The PR sends X and Y as two independent BusValue::Packed { packing: Packing::Direct } values. The LogUp fingerprint for the receiver is z - (X_bitwise + α·Y_bitwise), and the sender must match it. Since α is a random challenge unknown to the prover, Schwartz–Zippel guarantees X_cpu = X_bitwise and Y_cpu = Y_bitwise independently — and since every row of the precomputed BITWISE table has X, Y ∈ [0, 255], both bytes are proven in range. The constraint transformation is sound.

Medium — BusId renumbering is a silent protocol break

IsB20 was renumbered from 2 to 3, shifting every bus ID ≥ 3 by one (Commit goes from 21 to 22). TryFrom<u64> returns Err for value 2, leaving a hole. Any external verifier, serialized proof, or cross-version artifact using numeric bus IDs will silently misroute or hard-fail. If no persistent proof formats or external verifiers consume these IDs directly this is low-risk; otherwise a protocol version bump is needed.

Low — PR description off-by-one

The description says "reducing CPU bus interactions from 68 to 56 (-18%)" but the math and the test both give 55: 27 IS_BYTE → 14 IS_BYTE = −13 interactions; 68 − 13 = 55. The test in cpu_tests.rs correctly asserts 55.

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

Reviewed: byte pairing logic correctness, BusId renumbering consistency, bus interaction value counts, soundness of dual-byte IS_BYTE[X, Y] lookups, trace builder padding alignment, and PAGE/BRANCH single-byte (Y=0) convention.

🤖 Generated with Claude Code

_{- If this code review was useful, please react with 👍. Otherwise, react with 👎.}

Review: Perf/batch byte range checks

Overall: The batching optimization is sound. Pairing two byte columns into one IS_BYTE[X,Y] lookup is safe because the BITWISE table contains rows for every (x,y) in [0,255]x[0,255], so both values are individually constrained. The count drop from 68 to 55 CPU bus interactions checks out (27 IS_BYTE to 14 = 13 fewer).

Medium - Unexplained BusId gap at value 2 (see inline comment on types.rs)

IsB20 is explicitly pinned to = 3, but nothing is inserted at position 2. This makes TryFrom(2) return Err(2) where it previously returned IsB20, and shifts every channel ID from IsB20 onward by +1 (AndByte 3->4, Commit 21->22) - a protocol-breaking change for stored proof artifacts. If slot 2 is intentionally reserved, document it. If unintentional, drop the = 3 so the numbering stays contiguous.

Low - PR description says 56 interactions, code says 55

The description states reducing CPU bus interactions from 68 to 56 (-18%) but cpu_tests.rs asserts interactions.len() == 55 (68 - 13 = 55). Minor doc discrepancy.

/bench 3

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

Notes (below threshold, informational only):

• The IS_BYTE soundness concern raised in the existing comment is a false positive for this PR. IS_BYTE sends X and Y as independent BusValue::Packed { packing: Direct } entries, producing separate alpha-weighted fingerprint terms. The BITWISE table only has rows where X,Y in [0,255], so both bytes are individually constrained. The IS_HALF packing confusion (lo+256*hi) does not apply here.

• PR description says "68 to 56 (-18%)" but the code and test correctly assert 55 interactions. Minor text discrepancy.

• single_byte doc comment (bitwise.rs:507) still lists IS_BYTE as a "single-byte op" example. This is technically still true (you CAN use single_byte(IsByte, x) with y=0), but could be clarified since IS_BYTE now primarily operates in two-byte mode via byte_op().

🤖 Generated with Claude Code

_{- If this code review was useful, please react with 👍. Otherwise, react with 👎.}

Review: Perf/batch byte range checks

The optimization is cryptographically sound. The BITWISE table already enumerates all 65536 (X, Y) byte pairs for AND/OR/XOR, so re-using those rows for IS_BYTE[X, Y] is valid - the LogUp fingerprint includes both values, so an out-of-range byte in either position has no matching table row and the proof fails. Multiplicity accounting looks consistent between bus_interactions(), collect_byte_check_ops(), and the padding helper (all produce 14 ops per CPU row: 1+1+12).

Issues:

Medium - Pre-existing test bug fixed here (inline on prove_elfs_tests.rs:1007): bus_id = 17 was BusId::Branch, not BusId::Memory (which is 16 in the enum). Good catch. Suggest using the named constant directly to prevent future drift.

Low - PR description says "68 to 56 (-18%)" but the assertion and its own arithmetic give 55 total (-19%). Minor doc fix needed.

No other issues found.

/bench 3